$\forall$${\it es}$:event\_system\{i:l\}, $e$:es{-}E(${\it es}$). es{-}le(${\it es}$; es{-}init(${\it es}$;$e$); $e$) $\Leftarrow\!\Rightarrow$ True